Inference at * 1 0 
Iof proof for Lemma integer sqrt:



1. n : 
  r:. (((r * r)  n) & (n < ((r+1) * (r+1)))) 

latex

 by (%S% \p.AbSetHD (get_int_arg `hn` p) p) 

latex

 1: 

 1: 1. n : 
 1: 2. n  0 
 1:   r:. (((r * r)  n) & (n < ((r+1) * (r+1))))
 .

Definitions	x:AB(x), A  B, {x:A| B(x)} , x:A. B(x), i  j , t  T,
Lemmas	nat properties